$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $f$:($T$$\rightarrow$$T$).
\\[0ex]retraction($T$;$f$) $\Rightarrow$ ($\forall$$x$, $y$:$T$. $x$ is $f$$\ast$($y$) $\Rightarrow$ ($f$$\ast\ast$($x$) = $f$$\ast\ast$($y$) $\in$ $T$))